Nuprl Lemma : sum_unroll_lo_q
11,40
postcript
pdf
i
,
j
:
. (
i
<
j
)
(
E
:({
i
..
j
}
).
i
k
<
j
.
E
(
k
) = (
E
(
i
) +
i
+1
k
<
j
.
E
(
k
))
)
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
+
r
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
,
a
j
<
b
.
E
(
j
)
Lemmas
crng
wf
,
qrng
wf
,
rng
sum
unroll
lo
origin
i, j:
. (i < j) 
(E:({i..j
}
). 
i 
k < j. E(k) = (E(i) + i+1 k < j. E(k)) 
) i, j:. (i < j) (E:({i..j}). i k < j. E(k) = (E(i) + i+1 k < j. E(k)) ) T+*>x:A. B(x)a j < b. E(j)